Definitions | filter(P;l), eventlist(pred?;e), sends-bound(p;e;l), SWellFounded(R(x;y)),  x,y. t(x;y), A & B, A, first(e), pred(e), x:A. B(x), rcv?(e), sender(e), link(e), P & Q, P Q, e < e', loc(e), destination(l), Id, Unit, IdLnk, EqDecider(T),  x. t(x), P  Q, receives(dE;dL;pred?;info;p;e;l), Prop, b, rcv-from-on(dE;dL;info;e;l;r), t T, x:A. B(x), x L. P(x) |